\begin{tabbing}
1. $T$ : Type
\\[0ex]2. ${\it T'}$ : Type
\\[0ex]3. $E$ : $T$$\rightarrow$$T$$\rightarrow\mathbb{P}$
\\[0ex]4. ${\it E'}$ : ${\it T'}$$\rightarrow$${\it T'}$$\rightarrow\mathbb{P}$
\\[0ex]5. $T$ = ${\it T'}$
\\[0ex]6. $\forall$$x$, $y$:$T$. $E$($x$,$y$) $\Leftarrow\!\Rightarrow$ ${\it E'}$($x$,$y$)
\\[0ex]$\vdash$  \=(($\forall$$a$:$T$. $E$($a$,$a$))\+
\\[0ex]\& ($\forall$$a$, $b$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$a$))
\\[0ex]\& ($\forall$$a$, $b$, $c$:$T$. $E$($a$,$b$) $\Rightarrow$ $E$($b$,$c$) $\Rightarrow$ $E$($a$,$c$)))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($\forall$$a$:${\it T'}$. ${\it E'}$($a$,$a$))\+
\\[0ex]\& ($\forall$$a$, $b$:${\it T'}$. ${\it E'}$($a$,$b$) $\Rightarrow$ ${\it E'}$($b$,$a$))
\\[0ex]\& ($\forall$$a$, $b$, $c$:${\it T'}$. ${\it E'}$($a$,$b$) $\Rightarrow$ ${\it E'}$($b$,$c$) $\Rightarrow$ ${\it E'}$($a$,$c$)))
\-\-
\end{tabbing}